Nuprl Definition : R-size 11,40

R-size(R)
== es_realizer_ind(R;
== es_realizer_ind(1;
== es_realizer_ind(left,right,rec1,rec2.(rec1 + rec2);
== es_realizer_ind(loc,T,x,v.1;
== es_realizer_ind(loc,T,x,L.1;
== es_realizer_ind(lnk,tag,L.1;
== es_realizer_ind(loc,ds,knd,T,x,f.1;
== es_realizer_ind(ds,knd,T,l,dt,g.1;
== es_realizer_ind(loc,ds,a,T,P.1;
== es_realizer_ind(loc,k,L.1;
== es_realizer_ind(loc,k,L.1;
== es_realizer_ind(loc,x,L.1) 
latex


Definitions#$n, n + m, es realizer ind
FDL editor aliasesR-size

origin